Nuprl Definition : es-bless
11,40
postcript
pdf
e
<loc
e'
== case TERMOF{
decidable
es-locl
:ObjectId, 1:l, i:l}(
es
,
e'
,
e
) of inl(
x
) => tt | inr(
x
) => ff
latex
clarification:
es-bless{i:l}
es-bless
(
es
;
e
;
e'
)
== case TERMOF{
decidable
es-locl
:ObjectId, 1:l, i:l}(
es
,
e'
,
e
) of inl(
x
) => tt | inr(
x
) => ff
latex
Definitions
decidable
es-locl
,
tt
,
ff
FDL editor aliases
es-bless
origin